

LEMMA

Tangential proper part implies proper part.
=============================
Step 1

? (all x (all y ((tpp x y) => (pp x y))))


> revsk
=============================
Step 2

? ((~ (tpp c1330697 c1330696)) v (pp c1330697 c1330696))


> hypdisj
=============================
Step 3

? (pp c1330697 c1330696)

1. (tpp c1330697 c1330696)

> ((pp X Y) <-- (tpp X Y))
=============================
Step 4

? (tpp c1330697 c1330696)

1. (~ (pp c1330697 c1330696))
2. (tpp c1330697 c1330696)

> hyp


LEMMA

Proper part implies parthood.
=============================
Step 1

? (all x (all y ((pp x y) => (p x y))))


> revsk
=============================
Step 2

? ((~ (pp c1335826 c1335825)) v (p c1335826 c1335825))


> hypdisj
=============================
Step 3

? (p c1335826 c1335825)

1. (pp c1335826 c1335825)

> ((p X Y) <-- (pp X Y))
=============================
Step 4

? (pp c1335826 c1335825)

1. (~ (p c1335826 c1335825))
2. (pp c1335826 c1335825)

> hyp


LEMMA

Parthood is transitive.
=============================
Step 1

? (all x (all y (all z (((p x y) & (p y z)) => (p x z)))))


> revsk
=============================
Step 2

? (((~ (p c1341013 c1341012)) v (~ (p c1341012 c1341011))) v (p c1341013 c1341011))


> hypdisj
=============================
Step 3

? (p c1341013 c1341011)

1. (p c1341012 c1341011)
2. (p c1341013 c1341012)

> ((p Z X) <-- (~ (c (f1335856 Z X Y) Z)))
=============================
Step 4

? (~ (c (f1335856 c1341013 c1341011 Var33) c1341013))

1. (~ (p c1341013 c1341011))
2. (p c1341012 c1341011)
3. (p c1341013 c1341012)

> ((~ (c Y X)) <-- (p X Z) (~ (c Y Z)))
|=============================
|Step 5
|
|? (p c1341013 Var36)
|
|1. (c (f1335856 c1341013 c1341011 Var33) c1341013)
|2. (~ (p c1341013 c1341011))
|3. (p c1341012 c1341011)
|4. (p c1341013 c1341012)
|
|> hyp
=============================
Step 6

? (~ (c (f1335856 c1341013 c1341011 Var33) c1341012))

1. (c (f1335856 c1341013 c1341011 Var33) c1341013)
2. (~ (p c1341013 c1341011))
3. (p c1341012 c1341011)
4. (p c1341013 c1341012)

> ((~ (c Y X)) <-- (p X Z) (~ (c Y Z)))
|=============================
|Step 7
|
|? (p c1341012 Var40)
|
|1. (c (f1335856 c1341013 c1341011 Var33) c1341012)
|2. (c (f1335856 c1341013 c1341011 Var33) c1341013)
|3. (~ (p c1341013 c1341011))
|4. (p c1341012 c1341011)
|5. (p c1341013 c1341012)
|
|> hyp
=============================
Step 8

? (~ (c (f1335856 c1341013 c1341011 Var33) c1341011))

1. (c (f1335856 c1341013 c1341011 Var33) c1341012)
2. (c (f1335856 c1341013 c1341011 Var33) c1341013)
3. (~ (p c1341013 c1341011))
4. (p c1341012 c1341011)
5. (p c1341013 c1341012)

> ((~ (c (f1335856 Y Z X) Z)) <-- (~ (p Y Z)))
=============================
Step 9

? (~ (p c1341013 c1341011))

1. (c (f1335856 c1341013 c1341011 Var33) c1341011)
2. (c (f1335856 c1341013 c1341011 Var33) c1341012)
3. (c (f1335856 c1341013 c1341011 Var33) c1341013)
4. (~ (p c1341013 c1341011))
5. (p c1341012 c1341011)
6. (p c1341013 c1341012)

> hyp


LEMMA

Parthood plus failure of converse parthood gives proper part.
=============================
Step 1

? (all x (all y (((p x y) & (~ (p y x))) => (pp x y))))


> revsk
=============================
Step 2

? (((~ (p c1346354 c1346353)) v (p c1346353 c1346354)) v (pp c1346354 c1346353))


> hypdisj
=============================
Step 3

? (pp c1346354 c1346353)

1. (~ (p c1346353 c1346354))
2. (p c1346354 c1346353)

> ((pp Y X) <-- (p Y X) (~ (p X Y)))
|=============================
|Step 4
|
|? (p c1346354 c1346353)
|
|1. (~ (pp c1346354 c1346353))
|2. (~ (p c1346353 c1346354))
|3. (p c1346354 c1346353)
|
|> hyp
=============================
Step 5

? (~ (p c1346353 c1346354))

1. (~ (pp c1346354 c1346353))
2. (~ (p c1346353 c1346354))
3. (p c1346354 c1346353)

> hyp


LEMMA

Proper part splits into tangential or non-tangential proper part.
=============================
Step 1

? (all x (all y ((pp x y) => ((tpp x y) v (ntpp x y)))))


> revsk
=============================
Step 2

? ((~ (pp c1351846 c1351845)) v ((tpp c1351846 c1351845) v (ntpp c1351846 c1351845)))


> hypdisj
=============================
Step 3

? (ntpp c1351846 c1351845)

1. (~ (tpp c1351846 c1351845))
2. (pp c1351846 c1351845)

> ((ntpp Z X) <-- (pp Z X) (~ (ec (f1346443 Z X Y) Z)))
|=============================
|Step 4
|
|? (pp c1351846 c1351845)
|
|1. (~ (ntpp c1351846 c1351845))
|2. (~ (tpp c1351846 c1351845))
|3. (pp c1351846 c1351845)
|
|> hyp
=============================
Step 5

? (~ (ec (f1346443 c1351846 c1351845 Var32) c1351846))

1. (~ (ntpp c1351846 c1351845))
2. (~ (tpp c1351846 c1351845))
3. (pp c1351846 c1351845)

> ((~ (ec X Y)) <-- (pp Y Z) (ec X Z) (~ (tpp Y Z)))
||=============================
||Step 6
||
||? (pp c1351846 Var36)
||
||1. (ec (f1346443 c1351846 c1351845 Var32) c1351846)
||2. (~ (ntpp c1351846 c1351845))
||3. (~ (tpp c1351846 c1351845))
||4. (pp c1351846 c1351845)
||
||> hyp
|=============================
|Step 7
|
|? (ec (f1346443 c1351846 c1351845 Var32) c1351845)
|
|1. (ec (f1346443 c1351846 c1351845 Var32) c1351846)
|2. (~ (ntpp c1351846 c1351845))
|3. (~ (tpp c1351846 c1351845))
|4. (pp c1351846 c1351845)
|
|> ((ec (f1346443 Y Z X) Z) <-- (~ (ntpp Y Z)) (pp Y Z))
||=============================
||Step 8
||
||? (~ (ntpp c1351846 c1351845))
||
||1. (~ (ec (f1346443 c1351846 c1351845 Var32) c1351845))
||2. (ec (f1346443 c1351846 c1351845 Var32) c1351846)
||3. (~ (ntpp c1351846 c1351845))
||4. (~ (tpp c1351846 c1351845))
||5. (pp c1351846 c1351845)
||
||> hyp
|=============================
|Step 9
|
|? (pp c1351846 c1351845)
|
|1. (~ (ec (f1346443 c1351846 c1351845 Var32) c1351845))
|2. (ec (f1346443 c1351846 c1351845 Var32) c1351846)
|3. (~ (ntpp c1351846 c1351845))
|4. (~ (tpp c1351846 c1351845))
|5. (pp c1351846 c1351845)
|
|> hyp
=============================
Step 10

? (~ (tpp c1351846 c1351845))

1. (ec (f1346443 c1351846 c1351845 Var32) c1351846)
2. (~ (ntpp c1351846 c1351845))
3. (~ (tpp c1351846 c1351845))
4. (pp c1351846 c1351845)

> hyp


LEMMA

From tpp(x,y) and tpp(y,z) get p(x,y) and p(y,z); by transitivity get p(x,z). Since z cannot be part of x, infer pp(x,z), then split to tpp(x,z) or ntpp(x,z).
=============================
Step 1

? (all x (all y (all z (((tpp x y) & (tpp y z)) => ((tpp x z) v (ntpp x z))))))


> revsk
=============================
Step 2

? (((~ (tpp c1357491 c1357490)) v (~ (tpp c1357490 c1357489))) v ((tpp c1357491 c1357489) v (ntpp c1357491 c1357489)))


> hypdisj
=============================
Step 3

? (ntpp c1357491 c1357489)

1. (~ (tpp c1357491 c1357489))
2. (tpp c1357490 c1357489)
3. (tpp c1357491 c1357490)

> ((ntpp X Y) <-- (pp X Y) (~ (tpp X Y)))
|=============================
|Step 4
|
|? (pp c1357491 c1357489)
|
|1. (~ (ntpp c1357491 c1357489))
|2. (~ (tpp c1357491 c1357489))
|3. (tpp c1357490 c1357489)
|4. (tpp c1357491 c1357490)
|
|> ((pp Y X) <-- (p Y X) (~ (p X Y)))
||=============================
||Step 5
||
||? (p c1357491 c1357489)
||
||1. (~ (pp c1357491 c1357489))
||2. (~ (ntpp c1357491 c1357489))
||3. (~ (tpp c1357491 c1357489))
||4. (tpp c1357490 c1357489)
||5. (tpp c1357491 c1357490)
||
||> ((p X Z) <-- (p X Y) (p Y Z))
|||=============================
|||Step 6
|||
|||? (p c1357491 Var54)
|||
|||1. (~ (p c1357491 c1357489))
|||2. (~ (pp c1357491 c1357489))
|||3. (~ (ntpp c1357491 c1357489))
|||4. (~ (tpp c1357491 c1357489))
|||5. (tpp c1357490 c1357489)
|||6. (tpp c1357491 c1357490)
|||
|||> ((p X Y) <-- (pp X Y))
|||=============================
|||Step 7
|||
|||? (pp c1357491 Var54)
|||
|||1. (~ (p c1357491 Var54))
|||2. (~ (p c1357491 c1357489))
|||3. (~ (pp c1357491 c1357489))
|||4. (~ (ntpp c1357491 c1357489))
|||5. (~ (tpp c1357491 c1357489))
|||6. (tpp c1357490 c1357489)
|||7. (tpp c1357491 c1357490)
|||
|||> ((pp X Y) <-- (tpp X Y))
|||=============================
|||Step 8
|||
|||? (tpp c1357491 Var54)
|||
|||1. (~ (pp c1357491 Var54))
|||2. (~ (p c1357491 Var54))
|||3. (~ (p c1357491 c1357489))
|||4. (~ (pp c1357491 c1357489))
|||5. (~ (ntpp c1357491 c1357489))
|||6. (~ (tpp c1357491 c1357489))
|||7. (tpp c1357490 c1357489)
|||8. (tpp c1357491 c1357490)
|||
|||> hyp
||=============================
||Step 9
||
||? (p c1357490 c1357489)
||
||1. (~ (p c1357491 c1357489))
||2. (~ (pp c1357491 c1357489))
||3. (~ (ntpp c1357491 c1357489))
||4. (~ (tpp c1357491 c1357489))
||5. (tpp c1357490 c1357489)
||6. (tpp c1357491 c1357490)
||
||> ((p X Y) <-- (pp X Y))
||=============================
||Step 10
||
||? (pp c1357490 c1357489)
||
||1. (~ (p c1357490 c1357489))
||2. (~ (p c1357491 c1357489))
||3. (~ (pp c1357491 c1357489))
||4. (~ (ntpp c1357491 c1357489))
||5. (~ (tpp c1357491 c1357489))
||6. (tpp c1357490 c1357489)
||7. (tpp c1357491 c1357490)
||
||> ((pp X Y) <-- (tpp X Y))
||=============================
||Step 11
||
||? (tpp c1357490 c1357489)
||
||1. (~ (pp c1357490 c1357489))
||2. (~ (p c1357490 c1357489))
||3. (~ (p c1357491 c1357489))
||4. (~ (pp c1357491 c1357489))
||5. (~ (ntpp c1357491 c1357489))
||6. (~ (tpp c1357491 c1357489))
||7. (tpp c1357490 c1357489)
||8. (tpp c1357491 c1357490)
||
||> hyp
|=============================
|Step 12
|
|? (~ (p c1357489 c1357491))
|
|1. (~ (pp c1357491 c1357489))
|2. (~ (ntpp c1357491 c1357489))
|3. (~ (tpp c1357491 c1357489))
|4. (tpp c1357490 c1357489)
|5. (tpp c1357491 c1357490)
|
|> ((~ (p Y X)) <-- (p X Z) (~ (p Y Z)))
||=============================
||Step 13
||
||? (p c1357491 Var67)
||
||1. (p c1357489 c1357491)
||2. (~ (pp c1357491 c1357489))
||3. (~ (ntpp c1357491 c1357489))
||4. (~ (tpp c1357491 c1357489))
||5. (tpp c1357490 c1357489)
||6. (tpp c1357491 c1357490)
||
||> ((p X Y) <-- (pp X Y))
||=============================
||Step 14
||
||? (pp c1357491 Var67)
||
||1. (~ (p c1357491 Var67))
||2. (p c1357489 c1357491)
||3. (~ (pp c1357491 c1357489))
||4. (~ (ntpp c1357491 c1357489))
||5. (~ (tpp c1357491 c1357489))
||6. (tpp c1357490 c1357489)
||7. (tpp c1357491 c1357490)
||
||> ((pp X Y) <-- (tpp X Y))
||=============================
||Step 15
||
||? (tpp c1357491 Var67)
||
||1. (~ (pp c1357491 Var67))
||2. (~ (p c1357491 Var67))
||3. (p c1357489 c1357491)
||4. (~ (pp c1357491 c1357489))
||5. (~ (ntpp c1357491 c1357489))
||6. (~ (tpp c1357491 c1357489))
||7. (tpp c1357490 c1357489)
||8. (tpp c1357491 c1357490)
||
||> hyp
|=============================
|Step 16
|
|? (~ (p c1357489 c1357490))
|
|1. (p c1357489 c1357491)
|2. (~ (pp c1357491 c1357489))
|3. (~ (ntpp c1357491 c1357489))
|4. (~ (tpp c1357491 c1357489))
|5. (tpp c1357490 c1357489)
|6. (tpp c1357491 c1357490)
|
|> ((~ (p Y X)) <-- (pp X Y))
|=============================
|Step 17
|
|? (pp c1357490 c1357489)
|
|1. (p c1357489 c1357490)
|2. (p c1357489 c1357491)
|3. (~ (pp c1357491 c1357489))
|4. (~ (ntpp c1357491 c1357489))
|5. (~ (tpp c1357491 c1357489))
|6. (tpp c1357490 c1357489)
|7. (tpp c1357491 c1357490)
|
|> ((pp X Y) <-- (tpp X Y))
|=============================
|Step 18
|
|? (tpp c1357490 c1357489)
|
|1. (~ (pp c1357490 c1357489))
|2. (p c1357489 c1357490)
|3. (p c1357489 c1357491)
|4. (~ (pp c1357491 c1357489))
|5. (~ (ntpp c1357491 c1357489))
|6. (~ (tpp c1357491 c1357489))
|7. (tpp c1357490 c1357489)
|8. (tpp c1357491 c1357490)
|
|> hyp
=============================
Step 19

? (~ (tpp c1357491 c1357489))

1. (~ (ntpp c1357491 c1357489))
2. (~ (tpp c1357491 c1357489))
3. (tpp c1357490 c1357489)
4. (tpp c1357491 c1357490)

> hyp
